María Inés de Frutos-Fernández

Given an ideal I in a commutative ring A, a divided power structure on I is a collection of maps {\gamma_n \colon I \to A}_n ∈\mathbbN, subject to axioms that imply that it behaves like the family {x \mapsto \fracx^nn!}_n ∈\mathbbN, but which can be defined even when division by factorials is not possible in A. Divided power structures have important applications in diverse areas of mathematics, including algebraic topology, number theory and algebraic geometry. In this article we describe a formalization in Lean 4 of the basic theory of divided power structures, including divided power morphisms and sub-divided power ideals, and we provide several fundamental constructions, in particular quotients and sums. This constitutes the first formalization of this theory in any theorem prover. As a prerequisite of general interest, we expand the formalized theory of multivariate power series rings, endowing them with a topology and defining evaluation and substitution of power series.

Local fields, and fields complete with respect to a discrete valuation, are essential objects in commutative algebra, with applications to number theory and algebraic geometry. We formalize in Lean the basic theory of discretely valued fields. In particular, we prove that the unit ball with respect to a discrete valuation on a field is a discrete valuation ring and, conversely, that the adic valuation on the field of fractions of a discrete valuation ring is discrete. We define finite extensions of valuations and of discrete valuation rings, and prove some global-to-local results. Building on this general theory, we formalize the abstract definition and some fundamental properties of local fields. As an application, we show that finite extensions of the field Q_p of p-adic numbers and of the field F_p((X)) of Laurent series over F_p are local fields.

The field R of real numbers is obtained from the rational numbers Q by taking the completion with respect to the usual absolute value. We then define the complex numbers C as an algebraic closure of R. The p-adic analogue of the real numbers is the field Q_p of p-adic numbers, obtained by completing Q with respect to the p-adic norm. In this paper, we formalize in Lean 3 the definition of the p-adic analogue of the complex numbers, which is the field C_p of p-adic complex numbers, a field extension of Q_p which is both algebraically closed and complete with respect to the extension of the p-adic norm. More generally, given a field K complete with respect to a nonarchimedean real-valued norm, and an algebraic field extension L/K, we show that there is a unique norm on L extending the given norm on K, with an explicit description. Building on the definition of C_p, we formalize the definition of the Fontaine period ring B_HT and discuss some applications to the theory of Galois representations and to p-adic Hodge theory. The results formalized in this paper are a prerequisite to formalize Local Class Field Theory, which is a fundamental ingredient of the proof of Fermat’s Last Theorem.

Let K/k be a finite Galois extension of global function fields. Let E be a Drinfeld module over k. We state and prove an equivariant refinement of Taelman’s analogue of the analytic class number formula for (E, K/k), and derive explicit consequences for the Galois structure of the Taelman class group of E over K.

We provide explicit equations for moduli spaces of Drinfeld shtukas over the projective line P^1 with Γ(N), Γ_1(N) and Γ_0(N) level structures, where N is an effective divisor on P^1. If the degree of N is high enough, these moduli spaces are relative surfaces. We study some invariants of the moduli space of shtukas with Γ_0(N) level structure for several degree 4 divisors on P^1.

The ring of adèles of a global field and its group of units, the group of idèles, are fundamental objects in modern number theory. We discuss a formalization of their definitions in the Lean 3 theorem prover. As a prerequisite, we formalize adic valuations on Dedekind domains. We present some applications, including the statement of the main theorem of global class field theory and a proof that the ideal class group of a number field is isomorphic to an explicit quotient of its idèle class group.